$\forall$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), $m$:Msg($M$). mval($m$) $\in$ $M$(mlnk($m$),mtag($m$))